(DEFPROP PROOFFNS
 (PROOFFNS PROOFMAX PROOFMIN PROOFMAXLIS PROOFMINLIS TER1 WIN1 SUCCESSORS1)
VALUE)

(DEFPROP PROOFMAX
 (LAMBDA(P)
  (COND	((TER1 (RECTIFY P)) (COND ((WIN1 (RECTIFY P)) (QUOTE (WIN))) (T (QUOTE LOSE))))
	(T (PROOFMAXLIS (SUCCESSORS1 (RECTIFY P))))))
EXPR)

(DEFPROP PROOFMIN
 (LAMBDA(P)
  (COND	((TER1 (RECTIFY P)) (COND ((WIN1 (RECTIFY P)) (QUOTE (WIN))) (T (QUOTE LOSE))))
	(T (PROOFMINLIS (SUCCESSORS1 (RECTIFY P))))))
EXPR)

(DEFPROP PROOFMAXLIS
 (LAMBDA(U)
  (COND	((NULL U) (QUOTE LOSE))
	(T
	 ((LAMBDA (X) (COND ((EQ X (QUOTE LOSE)) (PROOFMAXLIS (CDR U))) (T (CONS (CAR U) X))))
	  (PROOFMIN (CAR U))))))
EXPR)

(DEFPROP PROOFMINLIS
 (LAMBDA(U)
  (COND	((NULL U) NIL)
	(T
	 ((LAMBDA(X)
	   (COND ((EQ X (QUOTE LOSE)) (QUOTE LOSE))
		 (T
		  ((LAMBDA (Y) (COND ((EQ Y (QUOTE LOSE)) (QUOTE LOSE)) (T (CONS X Y))))
		   (PROOFMAXLIS (CDR U))))))
	  (PROOFMAX (CAR U))))))
EXPR)

(DEFPROP TER1
 (LAMBDA P (TER P (QUOTE (-20)) (QUOTE (20))))
EXPR)

(DEFPROP WIN1
 (LAMBDA (PP) (GREATERP (IMVAL PP (QUOTE (-20)) (QUOTE (20))) 0))
EXPR)

(DEFPROP SUCCESSORS1
 (LAMBDA (PP) (SUCCESSORS PP NIL NIL))
EXPR)